A:MsgA, x:Id, k:Knd, s1, s2:A.state, v:A.da(k).
ma-frame-compat(A;A)
 A.rframe(k reads x)
 (s1  s2 mod x)
 A.sends(k,s1,v) = A.sends(k,s2,v)  A.Msg List 

latex

Definitions

1of(t), tagged-messages(l;s;v;L), x:A. B(x), M.sends(k,s,v), P  Q, t  T, tagged-list-messages(s;v;L), S  T, Msg(da), Prop, A, False, 2of(t), SQType(T), x. t(x), {T}, T, x,y. t(x;y), True, M.Msg, Msg(M), AB, S  T, M.ds(x), (s1  s2 mod x), i  j < k, P & Q, {i..j}, x(s), M.state, , M.da(a), xdom(f). v=f(x)   P(x;v), P  Q, M.rframe(A.pre p for a), State(ds), M.rframe(k reads x), x(s1,s2), Valtype(da;k), ma-frame-compat(A;B), MsgA, M.sframe(k sends <l,tg>), z != f(x)  P(a;z), M.rframe(A.effect f of k on y), M.rframe(A.sends tfL of k on l), M.aframe(k affects x), M.frame(k affects x), P  Q, P  Q, Dec(P), M.dout(l,tg), (x  l), A & B, x:A. B(x), a = b

Lemmas

pi1 wf, Msg wf, not wf, fpf-vals wf, eqof wf, Knd wf, map equal, eq knd wf, fpf-cap wf, Knd sq, length wf1, Id wf, map wf, nat wf, idlnk-deq wf, ma-Msg wf, subtype rel list, true wf, tagged-messages wf, pi2 wf, ma-x-equiv wf, msga wf, assert wf, ma-st wf, select wf, concat wf, ma-da wf, id-deq wf, squash wf, IdLnk wf, Kind-deq wf, product-deq wf, ma-rframe wf, ma-frame-compat wf, assert-eq-knd, mlnk wf, top wf, rcv wf, l member wf, member-fpf-vals2, fpf-trivial-subtype-top, fpf-dom wf, decidable assert, select member, le wf, fpf-ap wf, deq wf, fpf wf